Nuprl Definition : weak-send-do-apply
11,40
postcript
pdf
weak-send-do-apply(
es
;
T
;
l
;
tg
;
a
;
ds
;
f
)
== discrete-weak-precond-send-p(
es
;
T
;{0..1
};
l
;
tg
;
a
;
ds
;
s
.can-apply(
f
;
s
);
s
,
v
. do-apply(
f
;
s
))
latex
Definitions
discrete-weak-precond-send-p(
es
;
T
;
A
;
l
;
tg
;
a
;
ds
;
P
;
f
)
,
{
i
..
j
}
,
#$n
,
can-apply(
f
;
x
)
,
x
.
A
(
x
)
,
do-apply(
f
;
x
)
FDL editor aliases
weak-send-do-apply
origin
};l;tg;a;ds;
s.can-apply(f;s);s,v. do-apply(f;s)) };l;tg;a;ds;s.can-apply(f;s);s,v. do-apply(f;s)) }x.A(x)